<style>
body {font-family: "lucida grande", lucida, verdana, sans-serif;}
body {margin: 20px 50px 0px 50px;}
body {background: #f5f5f5;}
body {line-height: 150%;}
a, a:link, a:visited {text-decoration: none; color: #0082ae;}
a:hover {border-color: #0082ae; border-width: 0 0 1px 0; border-style: solid;}
h1, h2, h3 {color: #A00; padding-top:15px;}
code, pre {font-size: 110%;}
table {border-collapse: collapse; }
td {border:1px solid #a1a5a9; padding:10px; font-size: 90%; vertical-align: top;}
span.lastchanged {color: #AAA; font-size: 20%; }
</style>

<html>
<body>

<h1><a href="http://www.cs.utwente.nl/~ruys/moonwalker/">
    MoonWalker</a></h1>

MoonWalker is a software model checker for CIL bytecode, the bytecode
of .NET programs.
MoonWalker is able to detect deadlocks and assertion violations in CIL programs. 
MoonWalker has been developed on the <a href="http://www.mono-project.com">
Mono platform</a>. 
The design of MoonWalker is inspired by and based on the 
<a href="http://javapathfinder.sourceforge.net/">
Java PathFinder (JPF)</a>, a model checker for Java programs. <br><br>

MoonWalker was previously known as MMC, the Mono Model Checker.
Due to several name clashes, however, the name of the software model 
checker has been changed to MoonWalker. <br><br>

MoonWalker has been developed in the <a href="http://fmt.cs.utwente.nl/">
Formal Methods and Tools</a> (FMT) group of the 
<a href="http://www.utwente.nl">University of Twente</a>. <br>
Contact person for MoonWalker: <a href="http://www.cs.utwente.nl/~ruys/">Theo Ruys</a>. <br>


<h2>Files</h2>

This binary distribution of MoonWalker 1.0.1 contains the following files:

<ul>
  <li><code>README.html</code>: this file</li>
  <li><code>LICENSE.txt</code>: Apache 2.0 license</li>
  <li><code>bin/moonwalker.exe</code>: MoonWalker executable</li>
  <li><code>bin/Mono.Cecil.dll</code>: Mono's 
      <a href="http://www.mono-project.com/Cecil">Cecil</a> library
      (version 0.6), needed by MoonWalker. </li>
  <li><code>bin/C5*</code>: 
      <a href="http://www.itu.dk/research/c5/">C5</a> library
      (version 1.0.2), needed by MoonWalker. </li>
  <li><code>examples/*.cs</code>: some C# examples</li>
</ul>

MoonWalker 1.0.1 has been compiled with Mono 1.2.6 under Mac OS X 10.4.11.


<h2>Installation</h2>

MoonWalker has been developed under Mono and Windows XP/Vista. <br>
Being a CIL assembly, MoonWalker should work on Windows XP/Vista
and on all Mono platforms. <br>

The <code>bin</code> directory of the binary distribution contains
all files needed to run MoonWalker. The <code>moonwalker.exe</code>
file can be installed anywhere, as long as both <code>*.dll</code>
files are placed in the same directory.


<h2>Running MoonWalker</h2>

First, compile a C# source program to CIL bytecode, e.g. using
Mono's C# compiler:
<pre>
    mcs Deadlock.cs
</pre>

If the C# program contains assertion checks, compile the model with 
<code>-d:DEBUG</code>, otherwise the assertion checks are not compiled 
into the resulting assembly. <br>

Next, run MoonWalker on the generated CIL bytecode:
<pre>
    mono moonwalker.exe -a Deadlock.exe
</pre>
If MoonWalker finds an error in the program (i.e. a deadlock or
assertion violation) it will write a trace leading to the error
into a file with extension <code>.trace</code> (in the above 
example this would be <code>Deadlock.exe.trace</code>).

A useful extra option to MoonWalker is <code>-s</code> which shows 
statistics on the verification run. <br>
To get a list of all supported options:
<pre>
    mono moonwalker.exe -h
</pre>


<h2>Licenses</h2>

MoonWalker itself is released under the
<a href="http://www.apache.org/licenses/LICENSE-2.0.html">
Apache 2.0 license</a>. <br>

Cecil is a Mono class library which is released under the 
<a href=http://www.opensource.org/licenses/mit-license.php>MIT X11 license</a>. <br>

C5 is released under a 
<a href="http://www.itu.dk/research/c5/LICENSE.txt">
MIT-style open license</a>. 

<h2>Version history</h2>

<table>
<tr><td>1.0.1</td>   
    <td>2008.04.11</td>     
    <td>First public release of MoonWalker (binary and <em>source</em>).</td>
</tr>
<tr><td>1.0.0</td>   
    <td>2007.12.19</td>     
    <td>New version after MSc Project by Viet Yen Nguyen. <br>
        Much improved performance due to optimisations like, e.g. ,
        dynamic partial order reduction, memoised garbage collection, 
        structured exception handling mechanism.</td>
</tr>
<tr><td>0.5.5</td>   
    <td>2007.03.28</td>     
    <td>Bytecode 2007 version: improved error trace + state information.</td>
</tr>
<tr><td>0.5.1</td>   
    <td>2006.12.18</td>     
    <td>First public release (binary only).</td>
</tr>
<tr><td>0.5</td>   
    <td>2006.08.28</td>     
    <td>Initial version after MSc Project of Niels Aan de Brugh.</td>
</tr>
</table>

<p>
<span class="lastchanged">
This page has last been updated by 
<a href="http://www.cs.utwente.nl/~ruys/">Theo Ruys</a>
on Friday, 11 April 2008.
</span>

</body>
</html>